(0) Obligation:
Clauses:
p(X, Y, Z) :- ','(=(X, Y), ','(=(Z, 1), !)).
p(X, Y, Z) :- ','(=(Z, 1), ','(=(Y, X), p(X, Y, Z))).
=(X, X).
Query: p(a,a,a)
(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)
Renamed defined predicates conflicting with built-in predicates [PROLOG].
(2) Obligation:
Clauses:
p(X, Y, Z) :- ','(user_defined_=(X, Y), ','(user_defined_=(Z, 1), !)).
p(X, Y, Z) :- ','(user_defined_=(Z, 1), ','(user_defined_=(Y, X), p(X, Y, Z))).
user_defined_=(X, X).
Query: p(a,a,a)
(3) PrologToPrologProblemTransformerProof (SOUND transformation)
Built Prolog problem from termination graph ICLP10.
(4) Obligation:
Clauses:
pA(T60).
pB(T15, T15, 1).
pB(T51, T51, 1) :- pA(T51).
pB(T92, T92, 1) :- pA(T92).
Query: pB(a,a,a)
(5) PrologToPiTRSProof (SOUND transformation)
We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
pB_in: (f,f,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
pB_in_aaa(T15, T15, 1) → pB_out_aaa(T15, T15, 1)
pB_in_aaa(T51, T51, 1) → U1_aaa(T51, pA_in_a(T51))
pA_in_a(T60) → pA_out_a(T60)
U1_aaa(T51, pA_out_a(T51)) → pB_out_aaa(T51, T51, 1)
pB_in_aaa(T92, T92, 1) → U2_aaa(T92, pA_in_a(T92))
U2_aaa(T92, pA_out_a(T92)) → pB_out_aaa(T92, T92, 1)
The argument filtering Pi contains the following mapping:
pB_in_aaa(
x1,
x2,
x3) =
pB_in_aaa
pB_out_aaa(
x1,
x2,
x3) =
pB_out_aaa(
x3)
U1_aaa(
x1,
x2) =
U1_aaa(
x2)
pA_in_a(
x1) =
pA_in_a
pA_out_a(
x1) =
pA_out_a
U2_aaa(
x1,
x2) =
U2_aaa(
x2)
1 =
1
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(6) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
pB_in_aaa(T15, T15, 1) → pB_out_aaa(T15, T15, 1)
pB_in_aaa(T51, T51, 1) → U1_aaa(T51, pA_in_a(T51))
pA_in_a(T60) → pA_out_a(T60)
U1_aaa(T51, pA_out_a(T51)) → pB_out_aaa(T51, T51, 1)
pB_in_aaa(T92, T92, 1) → U2_aaa(T92, pA_in_a(T92))
U2_aaa(T92, pA_out_a(T92)) → pB_out_aaa(T92, T92, 1)
The argument filtering Pi contains the following mapping:
pB_in_aaa(
x1,
x2,
x3) =
pB_in_aaa
pB_out_aaa(
x1,
x2,
x3) =
pB_out_aaa(
x3)
U1_aaa(
x1,
x2) =
U1_aaa(
x2)
pA_in_a(
x1) =
pA_in_a
pA_out_a(
x1) =
pA_out_a
U2_aaa(
x1,
x2) =
U2_aaa(
x2)
1 =
1
(7) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
PB_IN_AAA(T51, T51, 1) → U1_AAA(T51, pA_in_a(T51))
PB_IN_AAA(T51, T51, 1) → PA_IN_A(T51)
PB_IN_AAA(T92, T92, 1) → U2_AAA(T92, pA_in_a(T92))
The TRS R consists of the following rules:
pB_in_aaa(T15, T15, 1) → pB_out_aaa(T15, T15, 1)
pB_in_aaa(T51, T51, 1) → U1_aaa(T51, pA_in_a(T51))
pA_in_a(T60) → pA_out_a(T60)
U1_aaa(T51, pA_out_a(T51)) → pB_out_aaa(T51, T51, 1)
pB_in_aaa(T92, T92, 1) → U2_aaa(T92, pA_in_a(T92))
U2_aaa(T92, pA_out_a(T92)) → pB_out_aaa(T92, T92, 1)
The argument filtering Pi contains the following mapping:
pB_in_aaa(
x1,
x2,
x3) =
pB_in_aaa
pB_out_aaa(
x1,
x2,
x3) =
pB_out_aaa(
x3)
U1_aaa(
x1,
x2) =
U1_aaa(
x2)
pA_in_a(
x1) =
pA_in_a
pA_out_a(
x1) =
pA_out_a
U2_aaa(
x1,
x2) =
U2_aaa(
x2)
1 =
1
PB_IN_AAA(
x1,
x2,
x3) =
PB_IN_AAA
U1_AAA(
x1,
x2) =
U1_AAA(
x2)
PA_IN_A(
x1) =
PA_IN_A
U2_AAA(
x1,
x2) =
U2_AAA(
x2)
We have to consider all (P,R,Pi)-chains
(8) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PB_IN_AAA(T51, T51, 1) → U1_AAA(T51, pA_in_a(T51))
PB_IN_AAA(T51, T51, 1) → PA_IN_A(T51)
PB_IN_AAA(T92, T92, 1) → U2_AAA(T92, pA_in_a(T92))
The TRS R consists of the following rules:
pB_in_aaa(T15, T15, 1) → pB_out_aaa(T15, T15, 1)
pB_in_aaa(T51, T51, 1) → U1_aaa(T51, pA_in_a(T51))
pA_in_a(T60) → pA_out_a(T60)
U1_aaa(T51, pA_out_a(T51)) → pB_out_aaa(T51, T51, 1)
pB_in_aaa(T92, T92, 1) → U2_aaa(T92, pA_in_a(T92))
U2_aaa(T92, pA_out_a(T92)) → pB_out_aaa(T92, T92, 1)
The argument filtering Pi contains the following mapping:
pB_in_aaa(
x1,
x2,
x3) =
pB_in_aaa
pB_out_aaa(
x1,
x2,
x3) =
pB_out_aaa(
x3)
U1_aaa(
x1,
x2) =
U1_aaa(
x2)
pA_in_a(
x1) =
pA_in_a
pA_out_a(
x1) =
pA_out_a
U2_aaa(
x1,
x2) =
U2_aaa(
x2)
1 =
1
PB_IN_AAA(
x1,
x2,
x3) =
PB_IN_AAA
U1_AAA(
x1,
x2) =
U1_AAA(
x2)
PA_IN_A(
x1) =
PA_IN_A
U2_AAA(
x1,
x2) =
U2_AAA(
x2)
We have to consider all (P,R,Pi)-chains
(9) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 3 less nodes.
(10) TRUE